perm filename SUBSUM.NEW[1,JRA] blob sn#005866 filedate 1972-09-25 generic text, type T, neo UTF8
00100	
00200	
00300	(DEFPROP ATTEMPT 
00400	 (LAMBDA(L S C)
00500	  (PROG (NEWNAME SUPPORT
00600	 		 UNITPF
00700	 		 LCL
00800	 		 LVL
00900	 		 CNT
01000	 		 XYZ2
01100	 		 LSTCLS
01200	 		 LLST
01300	 		 Z1
01400	 		 MERGE
01500	 		 ORDER
01600	 		 DEBUG
01700	 		 DEPTH
01800	 		 LENGTH
01900	 		 ANCESTRY
02000	 		 STRATEGY
02100	 		 STRAT
02200	 		 PMODEL
02300	 		 NMODEL
02400	 		 PFLG
02500	 		 EQUAL
02600	 		 PDEPTH
02700	 		 DLIST
02800	 		 XYZ
02900	 		 XYZ1
03000	 		 COND
03100	 		 Z
03200	 		 UNAXP
03300	 		 UNAXN
03400	 		 SAT
03500	 		 EXTERM
03600	 		 EE
03700	 		 EE1
03800	 		 XX
03900	 		 CLAUSES
04000	 		 SUBCLAUSES
04100	 		 COUNT
04200	 		 SLENGTH
04300	 		 ORDLST
04400	 		 OCLIST)
04500		(SETQ NEWNAME (LIST (LIST NIL)))
04600		(SETORD (CAR L) (CDR L))
04700		(SETQ Z (MINIMIZE (CAR L)))
04800		(UPDATESTATE (COND ((NULL S) (SETQ STRAT (SETQUERY Z))) (T (SETQ STRAT S))))
04900		(SETQ COND C)
05000		(SETQ XYZ2 Z)
05100		(SETQ LVL 1)
05200		(SETQ COUNT 0)
05300		(SETQ Z (UNITPN XYZ2))
05400		(SETQ UNAXP (CAR Z))
05500		(SETQ UNAXN (CDR Z))
05600		(SETQ CLAUSES XYZ2)
05700		(COND ((NOT PFLG) (SETQ UNAXP (CONS (SET2 (LIST (LIST 1 NIL) (LIST EQUAL 0 0))) UNAXP))
05800				  (SETQ SUBCLAUSES (CONS (CAR UNAXP) CLAUSES)))
05900		      (T (SETQ SUBCLAUSES CLAUSES)))
06000		(SETQ LCL (LAST CLAUSES))
06100		(SETQ LSTCLS LCL)
06200		(COND (ANCESTRY (GO AA)))
06300		(SETQ XX (CONS CLAUSES CLAUSES))
06400		(SETQ EE CLAUSES)
06500		(SETQ EE1 (LAST EE))
06600		(SETQ CNT (LENGTH XYZ2))
06700	   BB   (SETQ Z1 (ERRSET (ATTEMPT1 XYZ2)))
06800		(COND ((OR (EQ Z1 (QUOTE NOPROOF)) (NULL Z1)) (RETURN (CONS (QUOTE NOPROOF) (CONS CLAUSES STRAT))))
06900		      ((EQ (CAR Z1) (QUOTE QED)) (SETQ Z
07000						       (EVAL
07100							(LIST (QUOTE OUTC)
07200							      (LIST (QUOTE OUTPUT) (QUOTE PRF) (QUOTE DSK:) FILENAM)
07300	 						      NIL)))
07400						 (QUERY)
07500						 (PROOF LHP RHP)
07600						 (OUTC Z T)
07700						 (RETURN Z1))
07800		      (T (RETURN Z1)))
07900	   AA   (SETQ XYZ XYZ2)
08000		(SETQ EE CLAUSES)
08100		(SETQ EE1 (LAST CLAUSES))
08200	   CC   (SETQ LLST (CONS (CAR XYZ) LLST))
08300		(SETQ XYZ (CDR XYZ))
08400		(COND (XYZ (GO CC)) (T (GO BB))))) 
08500	EXPR)
08600	
08700	(DEFPROP EDIT 
08800	 (LAMBDA(U Z)
08900	  (PROG (RES1 U1 U4 U5)
09000	   ED4  (COND ((NULL Z) (RETURN RES1)))
09100		(SETQ U4 (CAR Z))
09200		(SETQ U5 (CDR U4))
09300		(COND ((OR (GREATERP (NUM U4) LENGTH) (GREATERP (DEPTH U5) DEPTH)) (GO ED2)))
09400		(SETQ U1 SUBCLAUSES)
09500	ED1 
09600		(COND ((SUBSUME (CAR U1) U4) (GO ED2)))
09700	   ED6  (SETQ U1 (CDR U1))
09800		(COND (U1 (GO ED1)))
09900		(SETQ U1 (CDR Z))
10000		(COND ((NULL U1) (GO ED5)))
10100	   ED3  (COND ((SUBSUME (CAR U1) U4) (GO ED2)))
10200	   ED7  (SETQ U1 (CDR U1))
10300		(COND (U1 (GO ED3)))
10400	   ED5  (SETQ RES1 (CONS U4 RES1))
10500	   ED2  (SETQ Z (CDR Z))
10600		(GO ED4))) 
10700	EXPR)
10800	
10900	(DEFPROP SUBSUME 
11000	 (LAMBDA(C D)
11100	  (COND ((OR (AND (ALLPOS C) (ALLNEG D)) (AND (ALLNEG C) (ALLPOS D))) NIL)
11200		((OR (NOT (HERE C)) (NOT (HERE D))) NIL)
11300		((NOT (GREATERP (NUM C) (NUM D))) (SUBSUME1 (CDR C) (POSBIT C) (CDR D) (POSBIT D) NIL))
11400		(T NIL))) 
11500	EXPR)